Nuprl Lemma : ma-single-init_wf
11,40
postcript
pdf
x
:Id,
t
:Type,
v
:(
t
).
x
:
t
initially
x
=
v
MsgA
latex
Definitions
t
T
,
a
:
A
fp
B
(
a
)
,
Id
,
Type
,
x
:
v
,
MsgA
,
x
:
t
initially
x
=
v
,
mk-ma
,
suptype(
S
;
T
)
,
S
T
,
x
:
A
.
B
(
x
)
,
,
,
State(
ds
)
,
x
:
A
B
(
x
)
,
Top
,
x
:
A
B
(
x
)
,
IdLnk
,
,
type
List
,
f
(
x
)?
z
,
IdDeq
,
t
.2
,
x
.
t
(
x
)
,
x
:
A
.
B
(
x
)
,
x
.
A
(
x
)
,
Knd
,
Void
Lemmas
Knd
wf
,
Id
wf
,
pi2
wf
,
id-deq
wf
,
fpf-cap
wf
,
fpf-single
wf
,
fpf-empty
wf
,
IdLnk
wf
,
top
wf
,
ma-state
wf
,
rationals
wf
,
fpf-cap-single1
,
mk-ma
wf
origin
x:Id, t:Type, v:(
t). x : t initially x = v 
MsgA x:Id, t:Type, v:(t). x : t initially x = v MsgA T B(a)
T
x:A.B(x)
B(x)
B(x)
x. t(x)x:A. B(x)x.A(x)